feat: explicit defeq attribute
#8419
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
… update on the branch
…a stage0 update on the branch" This reverts commit 9535f2e.
nomeata
added
the
changelog-language
github-actions
bot
added
the
changes-stage0
Rob23oba
reviewed
May 20, 2025
nomeata
force-pushed
the
joachim/dsimp-attr
branch
from
f694af3 to
88c553f
Compare
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 20, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 20, 2025
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
the
breaks-mathlib
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 20, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 20, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 21, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 21, 2025
leanprover-community-bot
added
builds-mathlib
github-actions
bot
added
the
changes-stage0
|
Here are the benchmark results for commit 827a75f. |
|
!bench |
nomeata
force-pushed
the
joachim/dsimp-attr
branch
from
f89aad0 to
1f2edc1
Compare
|
Here are the benchmark results for commit f89aad0. Benchmark Metric Change
=================================================================================
+ Init.Data.BitVec.Lemmas re-elab branch-misses -2.1% (-39.1 σ)
+ Init.Data.List.Sublist re-elab -j4 branch-misses -2.6% (-23.5 σ)
+ Std.Data.DHashMap.Internal.RawLemmas branch-misses -3.6% (-48.3 σ)
+ binarytrees.st task-clock -9.3% (-21.5 σ)
+ binarytrees.st wall-clock -9.3% (-21.5 σ)
- bv_decide_inequality.lean maxrss 2.4% (192.9 σ)
- lake build no-op maxrss 7.0% (49.1 σ)
- riscv-ast.lean branches 2.4% (153.2 σ)
- riscv-ast.lean instructions 2.1% (73.4 σ)
+ stdlib blocked -96.3% (-1160.9 σ)
- stdlib blocked (unaccounted) 37.5% (33.8 σ) |
Rob23oba
reviewed
Jun 5, 2025
| def validateDefEqAttr (declName : Name) : AttrM Unit := do | ||
| let info ← getConstVal declName | ||
| MetaM.run' do | ||
| withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq` |
There was a problem hiding this comment.
If I understand this correctly,
def P := 1 = 1
@[defeq, simp]
theorem p_true : P := rflwould get accepted and then
/-
(kernel) application type mismatch: In the application
@id P True.intro
the final argument
True.intro
has type
True
but is expected to have type
P
-/
example : P := by dsimp(because it thinks P = True is defeq)
May have misunderstood how this attribute is supposed to work exactly though
There was a problem hiding this comment.
I get
def Q := 1 = 1
@[defeq, simp] theorem Q_true : Q := rfl
/-- error: dsimp made no progress -/
#guard_msgs in example : Q := by dsimp [Q_true]
on this branch (and also before).
I think this is expected: Q_true when used by simp is turned into eq_true Q_true : Q = True, and that isn't a rfl lemma.
There was a problem hiding this comment.
Hmm, that will make support for Iff a bit difficult though, won't it?
There was a problem hiding this comment.
Is this a regression, or are you worried about difficulties when adding new features? (I’m not worried about refactoring any of this after it lands.)
There was a problem hiding this comment.
Adding new features; but I guess yeah, it's fine to refactor so this can probably land like this for now.
nomeata
force-pushed
the
joachim/dsimp-attr
branch
from
1f2edc1 to
af15d77
Compare
|
!bench |
|
Here are the benchmark results for commit af15d77. Benchmark Metric Change
=================================================================================
- Init.Data.BitVec.Lemmas maxrss 16.1% (20.9 σ)
+ Init.Data.BitVec.Lemmas wall-clock -38.8% (-119.9 σ)
+ Init.Data.BitVec.Lemmas re-elab branches -2.4% (-89.4 σ)
+ Init.Data.BitVec.Lemmas re-elab instructions -2.3% (-95.2 σ)
+ Std.Data.DHashMap.Internal.RawLemmas wall-clock -13.4% (-32.3 σ)
- riscv-ast.lean branches 2.6% (58.8 σ)
- riscv-ast.lean instructions 2.3% (44.3 σ)
- stdlib attribute application 16.0% (56.6 σ)
+ stdlib blocked -93.4% (-1430.0 σ)
- stdlib tactic execution 8.7% (31.3 σ)
+ stdlib wall-clock -4.1% (-145.6 σ) |
This reverts commit b6838f8.
nomeata
force-pushed
the
joachim/dsimp-attr
branch
from
af15d77 to
8f798af
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 5, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 5, 2025
leanprover-community-bot
added
builds-mathlib
nomeata
force-pushed
the
joachim/dsimp-attr
branch
from
8f798af to
f6db92f
Compare
github-actions
bot
removed
the
changes-stage0
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces an explicit
defeqattribute to mark theorems that can be used bydsimp. The benefit of an explicit attribute over the prior logic of looking at the proof body is that we can reliably omit theorem bodies across module boundaries. It also helps with intra-file parallelism.If a theorem is syntactically defined by
:= rfl, then the attribute is assumed and need not given explicitly. This is a purely syntactic check and can be fooled, e.g. if in the current namespace,rflis not actually “the”rflofEq. In that case, some other syntax has be used, such as:= (rfl). This is also the way to go if a theorem can be proved bydefeq, but one does not actually wantdsimpto use this fact.The
defeqattribute will look at the type of the declaration, not the body, to check if it really holds definitionally. Because of different reduction settings, this can sometimes go wrong. Then one should also write:= (rfl), if one does not want this to be a defeq theorem. (If one does then this is currently not possible, but it’s probably a bad idea anyways).The
set_option debug.tactic.simp.checkDefEqAttr true,dsimpwill warn if could not apply a lemma due to a missingdefeqattribute.With
set_option backward.dsimp.useDefEqAttr.get falseone can revert to the old behavior of inferring rfl-ness based on the theorem body.Both options will go away eventually (too bad we can’t mark them as deprecated right away, see #7969)
Meta programs that generate theorems (e.g. equational theorems) can use
inferDefEqAttrto set the attribute based on the theorem body of the just created declaration.This builds on #8501 to update Init to
@[expose]a fair amount of definitions that, if not exposed, would prevent some existing:= rfltheorems from beingdefeqtheorems. In the interest of starting backwards compatible, I exposed these function. Hopefully many can be un-exposed later again.A mathlib adaption branch exists that includes both the meta programming fixes and changes to the theorems (e.g. changing
:= by rflto:= rfl).With the module system there is now no special handling for
defeqtheorem bodies, because we don’t look at the body anymore. The previous hack is removed. Thedefeq-ness of the theorem needs to be checked in the context of the theorem’s type; the error message contains a hint if the defeq check fails because of the exported context.